x,y:. ((x = y))  (x = y) 

latex

ProofTree

Definitions	, t  T, P  Q, P  Q, P  Q, P  Q, x:A. B(x), True, T, (i = j), if b then t else f fi , tt, b, P  Q, Dec(P), False, A, ff
Lemmas	eq int wf, assert wf, decidable int equal, bfalse wf, bool wf, true wf, squash wf, btrue wf